es:ES, P, Q:(E), T, T':Type, R:(TT').
(e:E. P(e)  (valtype(e) r T))
 (e:E. Q(e)  (valtype(e) r T'))
 (e.P(e) op e.Q(e) with R  ) 

latex

Definitions	e.P(e) op e'.Q(e') with R, x:A. B(x), P & Q, x:A  B(x), (e.P(e) a.f(a) e'.Q(e')) with R, a.f(a) is c preserving on e.P(e), x. t(x), {x:A| B(x)} , P  Q, x(s), f(a), valtype(e), x:AB(x), E, x:A. B(x), , Type, t  T, ES
Lemmas	event system wf, es-E wf, es-valtype wf, causale-order-preserving wf, causal-bijection wf